WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: goal(xs,ys) -> overlap(xs,ys) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() overlap(Cons(x,xs),ys) -> overlap[Ite][True][Ite](member(x,ys),Cons(x,xs),ys) overlap(Nil(),ys) -> False() - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() overlap[Ite][True][Ite](False(),Cons(x,xs),ys) -> overlap(xs,ys) overlap[Ite][True][Ite](True(),xs,ys) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,goal,member,member[Ite][True][Ite],notEmpty,overlap ,overlap[Ite][True][Ite]} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs goal#(xs,ys) -> c_1(overlap#(xs,ys)) member#(x,Nil()) -> c_2() member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')) notEmpty#(Cons(x,xs)) -> c_4() notEmpty#(Nil()) -> c_5() overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) overlap#(Nil(),ys) -> c_7() Weak DPs !EQ#(0(),0()) -> c_8() !EQ#(0(),S(y)) -> c_9() !EQ#(S(x),0()) -> c_10() !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y)) member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) member[Ite][True][Ite]#(True(),x,xs) -> c_13() overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) overlap[Ite][True][Ite]#(True(),xs,ys) -> c_15() and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: goal#(xs,ys) -> c_1(overlap#(xs,ys)) member#(x,Nil()) -> c_2() member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')) notEmpty#(Cons(x,xs)) -> c_4() notEmpty#(Nil()) -> c_5() overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) overlap#(Nil(),ys) -> c_7() - Weak DPs: !EQ#(0(),0()) -> c_8() !EQ#(0(),S(y)) -> c_9() !EQ#(S(x),0()) -> c_10() !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y)) member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) member[Ite][True][Ite]#(True(),x,xs) -> c_13() overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) overlap[Ite][True][Ite]#(True(),xs,ys) -> c_15() - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) goal(xs,ys) -> overlap(xs,ys) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() overlap(Cons(x,xs),ys) -> overlap[Ite][True][Ite](member(x,ys),Cons(x,xs),ys) overlap(Nil(),ys) -> False() overlap[Ite][True][Ite](False(),Cons(x,xs),ys) -> overlap(xs,ys) overlap[Ite][True][Ite](True(),xs,ys) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4,5} by application of Pre({4,5}) = {}. Here rules are labelled as follows: 1: goal#(xs,ys) -> c_1(overlap#(xs,ys)) 2: member#(x,Nil()) -> c_2() 3: member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')) 4: notEmpty#(Cons(x,xs)) -> c_4() 5: notEmpty#(Nil()) -> c_5() 6: overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) 7: overlap#(Nil(),ys) -> c_7() 8: !EQ#(0(),0()) -> c_8() 9: !EQ#(0(),S(y)) -> c_9() 10: !EQ#(S(x),0()) -> c_10() 11: !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y)) 12: member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) 13: member[Ite][True][Ite]#(True(),x,xs) -> c_13() 14: overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) 15: overlap[Ite][True][Ite]#(True(),xs,ys) -> c_15() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: goal#(xs,ys) -> c_1(overlap#(xs,ys)) member#(x,Nil()) -> c_2() member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')) overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) overlap#(Nil(),ys) -> c_7() - Weak DPs: !EQ#(0(),0()) -> c_8() !EQ#(0(),S(y)) -> c_9() !EQ#(S(x),0()) -> c_10() !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y)) member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) member[Ite][True][Ite]#(True(),x,xs) -> c_13() notEmpty#(Cons(x,xs)) -> c_4() notEmpty#(Nil()) -> c_5() overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) overlap[Ite][True][Ite]#(True(),xs,ys) -> c_15() - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) goal(xs,ys) -> overlap(xs,ys) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() overlap(Cons(x,xs),ys) -> overlap[Ite][True][Ite](member(x,ys),Cons(x,xs),ys) overlap(Nil(),ys) -> False() overlap[Ite][True][Ite](False(),Cons(x,xs),ys) -> overlap(xs,ys) overlap[Ite][True][Ite](True(),xs,ys) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:goal#(xs,ys) -> c_1(overlap#(xs,ys)) -->_1 overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys) ,member#(x,ys)):4 -->_1 overlap#(Nil(),ys) -> c_7():5 2:S:member#(x,Nil()) -> c_2() 3:S:member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')) -->_1 member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)):10 -->_2 !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y)):9 -->_1 member[Ite][True][Ite]#(True(),x,xs) -> c_13():11 -->_2 !EQ#(S(x),0()) -> c_10():8 -->_2 !EQ#(0(),S(y)) -> c_9():7 -->_2 !EQ#(0(),0()) -> c_8():6 4:S:overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) -->_1 overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)):14 -->_1 overlap[Ite][True][Ite]#(True(),xs,ys) -> c_15():15 -->_2 member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')):3 -->_2 member#(x,Nil()) -> c_2():2 5:S:overlap#(Nil(),ys) -> c_7() 6:W:!EQ#(0(),0()) -> c_8() 7:W:!EQ#(0(),S(y)) -> c_9() 8:W:!EQ#(S(x),0()) -> c_10() 9:W:!EQ#(S(x),S(y)) -> c_11(!EQ#(x,y)) -->_1 !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y)):9 -->_1 !EQ#(S(x),0()) -> c_10():8 -->_1 !EQ#(0(),S(y)) -> c_9():7 -->_1 !EQ#(0(),0()) -> c_8():6 10:W:member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) -->_1 member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')):3 -->_1 member#(x,Nil()) -> c_2():2 11:W:member[Ite][True][Ite]#(True(),x,xs) -> c_13() 12:W:notEmpty#(Cons(x,xs)) -> c_4() 13:W:notEmpty#(Nil()) -> c_5() 14:W:overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) -->_1 overlap#(Nil(),ys) -> c_7():5 -->_1 overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)):4 15:W:overlap[Ite][True][Ite]#(True(),xs,ys) -> c_15() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: notEmpty#(Nil()) -> c_5() 12: notEmpty#(Cons(x,xs)) -> c_4() 11: member[Ite][True][Ite]#(True(),x,xs) -> c_13() 9: !EQ#(S(x),S(y)) -> c_11(!EQ#(x,y)) 6: !EQ#(0(),0()) -> c_8() 7: !EQ#(0(),S(y)) -> c_9() 8: !EQ#(S(x),0()) -> c_10() 15: overlap[Ite][True][Ite]#(True(),xs,ys) -> c_15() * Step 4: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: goal#(xs,ys) -> c_1(overlap#(xs,ys)) member#(x,Nil()) -> c_2() member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')) overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) overlap#(Nil(),ys) -> c_7() - Weak DPs: member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) goal(xs,ys) -> overlap(xs,ys) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() overlap(Cons(x,xs),ys) -> overlap[Ite][True][Ite](member(x,ys),Cons(x,xs),ys) overlap(Nil(),ys) -> False() overlap[Ite][True][Ite](False(),Cons(x,xs),ys) -> overlap(xs,ys) overlap[Ite][True][Ite](True(),xs,ys) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:goal#(xs,ys) -> c_1(overlap#(xs,ys)) -->_1 overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys) ,member#(x,ys)):4 -->_1 overlap#(Nil(),ys) -> c_7():5 2:S:member#(x,Nil()) -> c_2() 3:S:member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')) -->_1 member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)):10 4:S:overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) -->_1 overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)):14 -->_2 member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')):3 -->_2 member#(x,Nil()) -> c_2():2 5:S:overlap#(Nil(),ys) -> c_7() 10:W:member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) -->_1 member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs)),!EQ#(x,x')):3 -->_1 member#(x,Nil()) -> c_2():2 14:W:overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) -->_1 overlap#(Nil(),ys) -> c_7():5 -->_1 overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) * Step 5: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: goal#(xs,ys) -> c_1(overlap#(xs,ys)) member#(x,Nil()) -> c_2() member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) overlap#(Nil(),ys) -> c_7() - Weak DPs: member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) goal(xs,ys) -> overlap(xs,ys) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() overlap(Cons(x,xs),ys) -> overlap[Ite][True][Ite](member(x,ys),Cons(x,xs),ys) overlap(Nil(),ys) -> False() overlap[Ite][True][Ite](False(),Cons(x,xs),ys) -> overlap(xs,ys) overlap[Ite][True][Ite](True(),xs,ys) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() goal#(xs,ys) -> c_1(overlap#(xs,ys)) member#(x,Nil()) -> c_2() member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) overlap#(Nil(),ys) -> c_7() overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) * Step 6: RemoveHeads WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: goal#(xs,ys) -> c_1(overlap#(xs,ys)) member#(x,Nil()) -> c_2() member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) overlap#(Nil(),ys) -> c_7() - Weak DPs: member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:goal#(xs,ys) -> c_1(overlap#(xs,ys)) -->_1 overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys) ,member#(x,ys)):4 -->_1 overlap#(Nil(),ys) -> c_7():5 2:S:member#(x,Nil()) -> c_2() 3:S:member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) -->_1 member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)):6 4:S:overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) -->_1 overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)):7 -->_2 member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))):3 -->_2 member#(x,Nil()) -> c_2():2 5:S:overlap#(Nil(),ys) -> c_7() 6:W:member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) -->_1 member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))):3 -->_1 member#(x,Nil()) -> c_2():2 7:W:overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) -->_1 overlap#(Nil(),ys) -> c_7():5 -->_1 overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)):4 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(1,goal#(xs,ys) -> c_1(overlap#(xs,ys)))] * Step 7: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: member#(x,Nil()) -> c_2() member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) overlap#(Nil(),ys) -> c_7() - Weak DPs: member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) and a lower component member#(x,Nil()) -> c_2() member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) overlap#(Nil(),ys) -> c_7() Further, following extension rules are added to the lower component. overlap#(Cons(x,xs),ys) -> member#(x,ys) overlap#(Cons(x,xs),ys) -> overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys) overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> overlap#(xs,ys) ** Step 7.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys),member#(x,ys)) -->_1 overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)):2 2:S:overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) -->_1 overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys) ,member#(x,ys)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys)) ** Step 7.a:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys)) overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- !EQ :: ["A"(0) x "A"(0)] -(0)-> "A"(13) 0 :: [] -(0)-> "A"(0) Cons :: ["A"(0) x "A"(8)] -(8)-> "A"(8) Cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) False :: [] -(0)-> "A"(1) False :: [] -(0)-> "A"(15) Nil :: [] -(0)-> "A"(0) S :: ["A"(0)] -(0)-> "A"(0) True :: [] -(0)-> "A"(1) True :: [] -(0)-> "A"(15) member :: ["A"(0) x "A"(0)] -(0)-> "A"(14) member[Ite][True][Ite] :: ["A"(1) x "A"(0) x "A"(0)] -(0)-> "A"(14) overlap# :: ["A"(8) x "A"(1)] -(6)-> "A"(1) overlap[Ite][True][Ite]# :: ["A"(1) x "A"(8) x "A"(1)] -(1)-> "A"(13) c_6 :: ["A"(1)] -(1)-> "A"(1) c_14 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "Cons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "False_A" :: [] -(0)-> "A"(1) "Nil_A" :: [] -(0)-> "A"(1) "S_A" :: ["A"(0)] -(0)-> "A"(1) "True_A" :: [] -(0)-> "A"(1) "c_14_A" :: ["A"(0)] -(0)-> "A"(1) "c_6_A" :: ["A"(0)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) 2. Weak: overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys)) ** Step 7.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys)) - Weak DPs: overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> c_14(overlap#(xs,ys)) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- !EQ :: ["A"(0) x "A"(0)] -(0)-> "A"(9) 0 :: [] -(0)-> "A"(0) Cons :: ["A"(10) x "A"(10)] -(10)-> "A"(10) Cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) False :: [] -(0)-> "A"(0) False :: [] -(0)-> "A"(1) False :: [] -(0)-> "A"(15) Nil :: [] -(0)-> "A"(0) S :: ["A"(0)] -(0)-> "A"(0) True :: [] -(0)-> "A"(0) True :: [] -(0)-> "A"(15) member :: ["A"(0) x "A"(0)] -(0)-> "A"(14) member[Ite][True][Ite] :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(14) overlap# :: ["A"(10) x "A"(15)] -(10)-> "A"(1) overlap[Ite][True][Ite]# :: ["A"(1) x "A"(10) x "A"(15)] -(0)-> "A"(13) c_6 :: ["A"(0)] -(0)-> "A"(12) c_14 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "Cons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "False_A" :: [] -(0)-> "A"(1) "Nil_A" :: [] -(0)-> "A"(1) "S_A" :: ["A"(1)] -(1)-> "A"(1) "True_A" :: [] -(0)-> "A"(1) "c_14_A" :: ["A"(0)] -(0)-> "A"(1) "c_6_A" :: ["A"(0)] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: overlap#(Cons(x,xs),ys) -> c_6(overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys)) 2. Weak: ** Step 7.b:1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: member#(x,Nil()) -> c_2() member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) overlap#(Nil(),ys) -> c_7() - Weak DPs: member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) overlap#(Cons(x,xs),ys) -> member#(x,ys) overlap#(Cons(x,xs),ys) -> overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys) overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> overlap#(xs,ys) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- !EQ :: ["A"(0) x "A"(0)] -(0)-> "A"(0) 0 :: [] -(0)-> "A"(0) Cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) False :: [] -(0)-> "A"(0) Nil :: [] -(0)-> "A"(0) S :: ["A"(0)] -(0)-> "A"(0) True :: [] -(0)-> "A"(0) member :: ["A"(0) x "A"(0)] -(0)-> "A"(0) member[Ite][True][Ite] :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) member# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) member[Ite][True][Ite]# :: ["A"(0) x "A"(0) x "A"(0)] -(1)-> "A"(0) overlap# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) overlap[Ite][True][Ite]# :: ["A"(0) x "A"(0) x "A"(0)] -(1)-> "A"(0) c_2 :: [] -(0)-> "A"(0) c_3 :: ["A"(0)] -(0)-> "A"(0) c_7 :: [] -(0)-> "A"(0) c_12 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: member#(x,Nil()) -> c_2() overlap#(Nil(),ys) -> c_7() 2. Weak: member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) ** Step 7.b:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) - Weak DPs: member#(x,Nil()) -> c_2() member[Ite][True][Ite]#(False(),x',Cons(x,xs)) -> c_12(member#(x',xs)) overlap#(Cons(x,xs),ys) -> member#(x,ys) overlap#(Cons(x,xs),ys) -> overlap[Ite][True][Ite]#(member(x,ys),Cons(x,xs),ys) overlap#(Nil(),ys) -> c_7() overlap[Ite][True][Ite]#(False(),Cons(x,xs),ys) -> overlap#(xs,ys) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) member(x,Nil()) -> False() member(x',Cons(x,xs)) -> member[Ite][True][Ite](!EQ(x,x'),x',Cons(x,xs)) member[Ite][True][Ite](False(),x',Cons(x,xs)) -> member(x',xs) member[Ite][True][Ite](True(),x,xs) -> True() - Signature: {!EQ/2,goal/2,member/2,member[Ite][True][Ite]/3,notEmpty/1,overlap/2,overlap[Ite][True][Ite]/3,!EQ#/2 ,goal#/2,member#/2,member[Ite][True][Ite]#/3,notEmpty#/1,overlap#/2,overlap[Ite][True][Ite]#/3} / {0/0 ,Cons/2,False/0,Nil/0,S/1,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1 ,c_13/0,c_14/1,c_15/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ#,goal#,member#,member[Ite][True][Ite]#,notEmpty# ,overlap#,overlap[Ite][True][Ite]#} and constructors {0,Cons,False,Nil,S,True} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- !EQ :: ["A"(0) x "A"(0)] -(0)-> "A"(12) 0 :: [] -(0)-> "A"(0) Cons :: ["A"(0) x "A"(9)] -(9)-> "A"(9) Cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Cons :: ["A"(0) x "A"(3)] -(3)-> "A"(3) False :: [] -(0)-> "A"(2) False :: [] -(0)-> "A"(0) False :: [] -(0)-> "A"(15) Nil :: [] -(0)-> "A"(0) Nil :: [] -(0)-> "A"(9) Nil :: [] -(0)-> "A"(3) S :: ["A"(0)] -(0)-> "A"(0) True :: [] -(0)-> "A"(2) True :: [] -(0)-> "A"(15) member :: ["A"(0) x "A"(0)] -(0)-> "A"(12) member[Ite][True][Ite] :: ["A"(2) x "A"(0) x "A"(0)] -(0)-> "A"(12) member# :: ["A"(0) x "A"(9)] -(9)-> "A"(4) member[Ite][True][Ite]# :: ["A"(0) x "A"(0) x "A"(9)] -(1)-> "A"(13) overlap# :: ["A"(3) x "A"(12)] -(6)-> "A"(2) overlap[Ite][True][Ite]# :: ["A"(0) x "A"(3) x "A"(12)] -(3)-> "A"(2) c_2 :: [] -(0)-> "A"(11) c_3 :: ["A"(0)] -(0)-> "A"(12) c_7 :: [] -(0)-> "A"(5) c_12 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "Cons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "False_A" :: [] -(0)-> "A"(1) "Nil_A" :: [] -(0)-> "A"(1) "S_A" :: ["A"(1)] -(1)-> "A"(1) "True_A" :: [] -(0)-> "A"(1) "c_12_A" :: ["A"(0)] -(0)-> "A"(1) "c_2_A" :: [] -(0)-> "A"(1) "c_3_A" :: ["A"(0)] -(0)-> "A"(1) "c_7_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: member#(x',Cons(x,xs)) -> c_3(member[Ite][True][Ite]#(!EQ(x,x'),x',Cons(x,xs))) 2. Weak: WORST_CASE(?,O(n^2))